p:IdLnk List. lpath(p)  Prop 

latex

Definitions	lpath(p), Id, destination(l), source(l), Prop, lnk-inv(l), l[i], x:A. B(x), {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, t  T, IdLnk
Lemmas	IdLnk wf, select wf, lnk-inv wf, not wf, lsrc wf, ldst wf, Id wf, length wf1, int seg wf